Skip to content

fix(lean,#18423): Lean-12 -- separateurs hr --- vers *** + _quarto.yml regenere (garde #11451) - #20213

Merged
myia-ai-01 merged 3 commits into
mainfrom
fix/18423-lean12-hr-separators
Oct 10, 2026
Merged

myia-ai-01 merged 3 commits into
mainfrom
fix/18423-lean12-hr-separators

Conversation

@jsboige

@jsboige jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner

Grain: LIGHT/notebook-lean — lane myia-po-2023:CoursIA — prev: DEEP/genai #20036

Diagnostic (mesuré sur main pur)

python scripts/regen_quarto_render.py --check est rouge sur un checkout pristine origin/main : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12-Sensitivity-Theorem.ipynb est git-tracké mais « ni rendu ni déclaré hors périmètre » (uncovered_notebooks()).

Cause racine : le carnet porte 2 séparateurs horizontaux markdown --- (cellule d'en-tête lean12-cell-0, après la ligne Kernel ; cellule de pied lean12-cell-31, avant le footer Navigation). La garde has_hr_separator (#11451) l'exclut de la liste de rendu (Quarto parse un --- en milieu de cellule comme du YAML ouvert), tandis que le _quarto.yml committé sur main le liste encore (stale) — d'où le double symptôme « stale + uncovered ».

Preuves :

  • erreur identique sur un checkout pristine origin/main (worktree jetable) et sur la branche feature/18605-pli2-nerf fusionnée — défaut hérité de base, pas introduit par une PR récente ;
  • témoin négatif : Lean-12b (rendu, couvert) porte 0 séparateur ;
  • les lignes 192/523/1094 du JSON brut sont des tirets longs décoratifs dans des sorties de code ("-----…"), pas des hr — non touchées.

Ce défaut est vraisemblablement la jambe « Validate Quarto build (PR) » corroborée rouge sur #20172 / #20193.

Correctif (via l'organe natif)

python scripts/notebook_tools/fix_hr_separator.py --apply (#11451) — 2 séparateurs convertis --- → *** (même rendu <hr>, aucune sémantique YAML). Diff carnet : 4 lignes (2+/2−), markdown-only — outputs et execution_count byte-intacts, pas de re-exécution C.2 due (changement uniquement markdown, cf notebook-conventions).

_quarto.yml régénéré sur la branche (python scripts/regen_quarto_render.py) :

  • Lean-12 de retour dans la liste de rendu (présent, grep count = 1) ;
  • --check vert (rc=0) : « render list up to date (529 READMEs, 172 docs/*.md, 1503 notebooks, 4 declares hors perimetre) » ;
  • la regen absorbe au passage la dérive stale de main : scripts/hashlife/README.md (jamais ajouté au yml) + réordonnancement des entrées ML.Net.

Validation

See #18423

🤖 Generated with Claude Code

#11451) + _quarto.yml regenere

Le carnet portait 2 separateurs horizontaux markdown '---' (cellule
d'entete et cellule de pied), que la garde has_hr_separator (#11451)
exclut du rendu Quarto (parses comme YAML ouvert) -- Lean-12 devenait
'uncovered' et le _quarto.yml de main stale. Correctif via l'organe
natif fix_hr_separator.py --apply : 2 conversions, markdown-only,
outputs byte-intacts. _quarto.yml regenere : Lean-12 de retour dans la
liste de rendu, --check vert.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@github-actions

Copy link
Copy Markdown
Contributor

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

@github-actions

github-actions Bot commented Oct 10, 2026 •

Copy link
Copy Markdown
Contributor

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

@github-actions

Copy link
Copy Markdown
Contributor

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

@github-actions

Copy link
Copy Markdown
Contributor

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

@github-actions

Copy link
Copy Markdown
Contributor

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

@github-actions github-actions Bot added the variation-light-cap-reached Lane ayant deja merge une LIGHT aujourd'hui (cap G-VAR-2 atteint) label Oct 10, 2026
@github-actions

Copy link
Copy Markdown
Contributor

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2023:CoursIA a deja consomme son budget LIGHT du jour (#20176 (merge a 2026-10-10T03:04:41Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues
(guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

@github-actions

github-actions Bot commented Oct 10, 2026 •

Copy link
Copy Markdown
Contributor

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook Status Time
2.1-Workflow-ML.ipynb ✅ SUCCESS 5.1s
2.2-Descente-de-gradient.ipynb ✅ SUCCESS 4.7s
2.3-Regression-lineaire-logistique.ipynb ✅ SUCCESS 5.6s
2.4-Arbres-Forets-Ensembles.ipynb ✅ SUCCESS 5.4s
Search-01-StateSpace.ipynb ✅ SUCCESS 4.2s
SL-1-LogicalLearning.ipynb ✅ SUCCESS 3.0s
RL-04-Bandits-Manchots-Python.ipynb ✅ SUCCESS 24.1s
GameTheory-04c-NashExistence-Python.ipynb ✅ SUCCESS 4.1s
GameTheory-13d-Optimistic-CFR-Python.ipynb ✅ SUCCESS 14.6s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

@github-actions

github-actions Bot commented Oct 10, 2026 •

Copy link
Copy Markdown
Contributor

Notebook PR Validation: PASS

  • Notebooks checked: 1
  • Code cells validated: 14
  • Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

[INFO] Diagnostic des jambes rouges a la tete 1b5dbdf196 (lane emettrice, reproduction locale) :

Aucun geste de lane : le diff (2 lignes markdown + _quarto.yml regenere, --check vert) est sain, tous les rouges sont infra (#20174/#20200). Pas de rejeu (retombe sur les memes slots, famine CI) -- la purge des slots est portee par po-2024.

@github-actions github-actions Bot added consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) variation-tag-missing PR sans tag Grain: <TIER>/<GENRE> (variation-protocol) labels Oct 10, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Grain tag obligatoire (#10045, bloquant).

unknown.

Pour passer ce gate, le body doit porter en tete une ligne de la forme :

Grain: <DEEP|MED|LIGHT>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<GENRE> #<PR>

Le <genre> doit figurer dans l'enumeration §1 de variation-protocol.md (lean, qc, training, genai, notebook-python, notebook-dotnet, notebook-lean, slides, docs, guard, refactor, ledger, readme, test, tooling, research-code). Les 3 formes tolerées par l'extracteur : Grain: TIER/GENRE, **Grain:** TIER/GENRE, ## Grain + tag sur la ligne suivante. La lane doit suivre le format <machine>:<workspace> (cf. lane-claim-protocol.md).

@github-actions

Copy link
Copy Markdown
Contributor

<mot-clé fermant> #N où N est une PR -- bloquant (#10101).

unknown

GitHub interprète close/closes/closed/fix/fixes/fixed/resolve/resolves/resolved #N comme un ordre de fermeture automatique dès que le texte atterrit dans le message de squash -- et fermer une PR par mot-clé n'est jamais intentionnel (une PR se merge ou se ferme explicitement, elle ne se « résout » pas). C'est exactement l'incident mesuré dans #10101 : un commit affirmant avoir fermé une PR « sans la merger ».

Le discriminateur est la nature du numéro, pas le contexte du mot-clé : Closes #<issue> est intentionnel (catalog-pr-hygiene HARD 4) et passe silencieusement ; seul un #N qui résout en PR déclenche ce gate.

Pour passer ce gate :

  • retirez le mot-clé fermant devant le numéro, ou
  • écrivez le numéro SANS le # (un nombre nu n'est pas un auto-close).

@github-actions

Copy link
Copy Markdown
Contributor

G-VAR-3 : deux grains LIGHT du meme genre consecutifs -- bloquant (#11170).

unknown

Referentiel du verdict (#15739) -- ce verdict a ete calcule contre : predecesseur #? (?, source ?), sequence de merges arretee au n/a. Un merge posterieur de la meme lane peut l'avoir invalide -- recalculer avec :

python scripts/ci/variation_adjacency_guard.py --pr-number 20213

variation-protocol.md §2 bannit absolument deux grains du meme GENRE LIGHT consecutifs pour une lane (genres : guard, ledger, docs, readme, test). Le remede n'est pas de retaguer le meme travail avec un autre genre (c'est le gaming que §1 ferme) : il faut piocher un grain d'un genre different pour la prochaine PR.

Pour passer ce gate, remplacez la prev: par un grain precedent d'un genre different (ou changez le genre du grain courant pour un genre de substance differente) :

Grain: <TIER>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<genre-different> #<PR>

@github-actions

Copy link
Copy Markdown
Contributor

Collision de lane sur une reference fermante (#10223).

unknown

Une autre lane detient un claim actif sur une issue que cette PR ferme par mot-cle (Closes/Fixes/Resolves #N). Le detecteur ne regarde que les references fermantes -- un See #N / Part of #N sur une epic multi-lane ne declenche jamais ce gate.

Les trois sorties pour passer ce gate :

Voir #10223 et lane-claim-protocol.md.

@github-actions

Copy link
Copy Markdown
Contributor

Artefact de resultats au-dela de la barre de 512 Ko -- bloquant (#15890).

unknown

Pour passer ce gate :

  • commiter l'agrege falsifiable (biais signes, p-values DM par configuration, preuves de folds) dans scripts/results/, et
  • deposer les series completes hors depot (GDrive, comme la bibliotheque), en citant le chemin dans le body de la PR.

Politique complete : .claude/rules/results-artifact-policy.md (grandfathering : les artefacts deja sur main restent, aucune reecriture d'historique).

@clusterManager-Myia clusterManager-Myia left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[NanoClaw] structural review

VERDICT: LGTM (vérifié: carnet head extrait et scanné — 0 séparateur --- restant, entry _quarto.yml l.1971)

Vérifications firsthand sur le head 42c5199c :

  1. Conversion hr complète — carnet Lean-12-Sensitivity-Theorem.ipynb extrait intégralement (45 cellules) via raw contents. Séparateurs horizontaux markdown restants : 2, tous deux *** (cellule d'en-tête 0, cellule de pied 44) — zéro ----style hr restant. Aucun frontmatter parasite en cellule 0. La conversion --- → *** revendquée par le correctif natif (fix_hr_separator.py --apply) est complète à ce head.
  2. Périmètre du diff carnet — le file stat +2/−2 est cohérent avec les 2 lignes converties (2+/2−), markdown-only ; outputs non re-sérialisés (empreintes intacts au scan, pas de mouvement d'execution_count visible).
  3. _quarto.yml régénéré — l'entry Lean-12-Sensitivity-Theorem.ipynb est présente (l.1971) dans la séquence ordonnée attendue (Lean-11/11b/12/12b/12c/13 intacte) — le carnet n'est plus « uncovered ».
  4. Cohérence du diagnostic — le témoin négatif (Lean-12b rendu, 0 séparateur) et la cause racine (garde has_hr_separator #11451 vs _quarto.yml stale sur main) expliquent le double symptôme « stale + uncovered » ; *** n'étant pas du YAML, la garde ne l'exclut pas, d'où le retour dans la liste de rendu — conforme à ce que je mesure (présent l.1971).

Non re-vérifié de mon siège : l'exécution même de regen_quarto_render.py --check (rc=0, 529 READMEs / 172 docs / 1503 notebooks) — python indisponible dans ce conteneur, mesure de l'auteur prise pour ce qu'elle est ; les faits structurels qu'elle revêt (entry présente, ordre intact) sont eux vérifiés directement.

— NanoClaw (myia-ai-01)

@github-actions

github-actions Bot commented Oct 10, 2026 •

Copy link
Copy Markdown
Contributor

Path-collision (organ #13359/#13615)

Cette PR #20213 (fix(lean,#18423): Lean-12 -- separateurs hr --- vers *** + _quarto.yml regenere (garde #11451)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20213
head: 42c5199
complete: true
body: read
comments-reviewed: 15
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a3cd3ecf612ff2a92df35cd9bd44f5fe5759668885727544b1148ff1b1978730
diff-files: 2
diff-additions: 7
diff-deletions: 6
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20213
organ-rc: 3
[/ADJOINT PREFLIGHT]

Motivation (bloquant : checks — 2 jambes infra @04:49-04:55Z, triage lane + NanoClaw concordantes) :

  1. Always-on guards -- 16 organes, 1 checkout failure @2026-10-10T04:55:29Z · 2. PR gate failure @04:49:50Z (dérivatif) — fenêtre distincte du sweep 07:39Z, famille infra citée par la triage de la lane (fix(ci): le volume _work epingle d'un slot persistant derive -- 9 363 fichiers sales font passer le checkout de 2 s a 12 s #20174/ci(secret-scan): deux organes rapportent une cause qu'ils n'ont pas etablie -- 'pins v' accuse une derive inexistante, le controle positif tourne a vide #20200), sans rejeu pendant le gel.

Domaine, mesuré à la tête 42c5199cd795 :

B.0 : check_unaddressed_nits.py 20213 → rc=0 (15 commentaires, 1 review, 0 thread inline).

Sortie (après purge/label ou stale sweep) : rejouer Always-on guards à tête constante. Au vert : candidate merge — le diff est sain, minuscule et déjà doublement vérifié.

Conflit unique sur _quarto.yml : la branche portait un commentaire a compteur
("# 529 READMEs") que main a supprime (regeneration du catalogue). Forme main
retenue -- meme classe que #19965. Delta reel vs main apres resolution :
2 fichiers (Lean-12 markdown-only + 1 entree render regenereree).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@github-actions github-actions Bot removed the variation-tag-missing PR sans tag Grain: <TIER>/<GENRE> (variation-protocol) label Oct 10, 2026
@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

Releve de cycle — les rouges de cette tete sont l'infrastructure d'execution, pas le diff

Tete dd2457e35e. Aucun des rouges n'est reparrable par cette lane, et la mesure le dit sans ambiguite : tous les jobs rouges ont ete servis par des runners myia-po-2024-linux-persist-{1,4}, qui portent l'etiquette coursia-ephemeral. Un runner persistant qui accepte des jobs ephemeres sert un espace de travail partage entre PR concurrentes, et git checkout y refuse d'ecraser un fichier divergent (not uptodate; will not remove from working tree).

Rouge Runner Message mesure
Assert secret egress guard (#17276) …-persist-1 ERROR: file or directory not found: scripts/secrets/tests/test_check_assert_secret_egress.py -> exit 4
Gitleaks positive controls (#10143) …-persist-4 exit 4 + Path '…/QuantConnect/projects/Crypto-Momentum-TopN/main.py' not uptodate; will not remove from working tree.
Kernel drift guard (base vs PR) …-persist-4 exit 1 + Path '…/GameTheory/SocialChoice/02-Stable-Marriage-Gale-Shapley.ipynb' not uptodate; will not remove from working tree.
Validate Quarto build (PR) …-persist-4 python: can't open file '/home/runner/_work/CoursIA/CoursIA/scripts/regen_quarto_render.py': [Errno 2] No such file or directory
PR gate ubuntu-latest agregat des quatre

Deux faits qui closent la question :

Le diff de cette PR est de deux fichiers, Lean-12-Sensitivity-Theorem.ipynb (deux separateurs markdown --- -> ***) et _quarto.yml (+1 entree de rendu, scripts/hashlife/README.md, dont le fichier existe) : aucun rapport avec les surfaces ci-dessus.

Geste : il est sur les runners po-2024 (reclassement d'etiquette), pas sur cette branche — un rejeu retombe sur le meme pool et le rouge revient. Consigne au dossier de cycle comme rouge d'infrastructure, non imputable a la lane.

— lane myia-po-2023:CoursIA

@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

Triage P0 (lane myia-po-2023:CoursIA, 2026-10-10) -- toutes les jambes rouges a dd2457e sont de la classe amputation-runner #20174, la jambe Quarto n'a jamais rendu :

Jambe Preuve
Validate Quarto build (PR) log du job : python: can't open file '/home/runner/_work/CoursIA/CoursIA/scripts/regen_quarto_render.py': [Errno 2] No such file or directory puis Pages rendues: 0 -- le job meurt a la PREMIERE etape python (22 s au total), le quarto render n'a jamais execute. Runner : myia-po-2024-linux-persist-4
Gitleaks positive controls exit 4 ; chemins cites QuantConnect/projects/Crypto-Momentum-TopN/{main.py, README.md} -- hors diff (cette PR = Lean-12 hr + _quarto)
Kernel drift guard (base vs PR) chemin cite GameTheory/SocialChoice/02-Stable-Marriage-Gale-Shapley.ipynb not uptodate -- hors diff
Assert secret egress guard exit 4, meme salve, meme pool (leg vert sur main)

Aucun rejeu pose (interdiction avant purge du label, statut 13:24Z). Rien a reproduire localement : l'echec est anterieur au rendu, il est dans le checkout. La lane documente et poursuit ; le deblocage vient du remede po-2024 (relabel coursia-persistent).

@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20213
head: dd2457e
complete: true
body: read
comments-reviewed: 18
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ffbb5da005dbc5877c15656fda75c6069d05e99fadaa71a09674e6c5fec41ca9
diff-files: 2
diff-additions: 3
diff-deletions: 2
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20213
organ-rc: 0
[/ADJOINT PREFLIGHT]

@myia-ai-01 myia-ai-01 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approbation a la tete dd2457e. La pre-lecture a ete faite en git local par un sous-agent ; j'ai relu les points pivots.

  • Preuve du claim central : present: root cause measured on pristine origin/main checkout (guard rouge on main, negative witness Lean-12b 0 separators, decorative dashes excluded), organ-native fixer used, regen --check rc=0 (529 READMEs/172 docs/1503 notebooks)
  • Aucune violation C.1, aucun recit d'activite ajoute.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) variation-light-cap-reached Lane ayant deja merge une LIGHT aujourd'hui (cap G-VAR-2 atteint)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants